es:ES, i:Id, L:(IdLnk List), T:(IdType).
es-secret-server{table:ut2, encrypt:ut2, decrypt:ut2}
es-secret-server(es; T; L; i)
 (e:E. (loc(e) = i)  (||"table" when e||  = ||"table" when es-init(es;e)||   )) 

latex

Definitions	secret-table(T), (state when e), s.x, , Top, e@i. P(e), x. t(x), t  T, "$x", P  Q, Id, x:A. B(x), P  Q, x:A. B(x), @i events of kind k change x to f State(ds) (val:T), xL. P(x), x(s), @i(x:T), @i only L affect x:T, A c B, , P & Q, let x = a in b(x), es-secret-server
Lemmas	data wf, int seg wf, es-val wf, es-vartype wf, es-when wf, st-length-encrypt, es-E wf, es-loc wf, es-kind wf, l member wf, member map, id-deq wf, fpf-cap-single1, event system wf, IdLnk wf, Id wf, es-secret-server wf, rcv wf, Knd wf, map wf, nat wf, st-length wf, secret-table wf, es-constant-1